'''
Created on 2011-04-25

@author: kacper
'''
from dataStructs.Transform import MultipleOr
from dataStructs.definitions import *
import subprocess
from parsing.parser import sents_parse_string
from dataStructs.exceptions import UnificationError



#f1 , f2 
def findUnify(MultOr1,MultOr2):
    f1 = MultOr1.fs
    f2 = MultOr2.fs
    
    return BrutefindUnify(f1,f2,[])
    
#f1, f2 lists of formulas 
def BrutefindUnify(f1,f2):

    for x in xrange(len(f1)):
        for y in xrange(len(f2)):
            try:
                sub =[]
                #because i am using equal  
                neg = f1[x].negFormula()
                #print "uni ", neg, f2[y]
                unify(neg,f2[y],sub)
                yield  (x,y)
            except UnificationError:
                pass
                 
 #           return BrutefindUnify(f1[1:], f2[:x]+f2[x+1:], subst+part_subst)
 
    


def BruteProgUnify(f1,f2):
    ags  = "prolog < uni.pl"
    file_object = open('uni.pl', 'w')

    file_object.write("a=b.\n")
    for x in xrange(len(f2)):
        for y in xrange(len(f1)):
    #        print f1[y] , "=" ,f2[x]
            file_object.write( "unify_with_occurs_check("+
                                str(f1[y]) + "," +str(f2[x]) +").\n")
    
    file_object.close()
            
    p = subprocess.Popen(ags, shell =True 
                         , stdout = subprocess.PIPE, stderr =  subprocess.PIPE);

    p.wait()
    comm= p.communicate()[1]
    
    
    comm = comm.split("\n")
    
    
    
    comm = filter(lambda x : x !="" , comm)[:-1]
   
    
    x=0
    while comm[x] != "false." : x +=1
    while x < len(comm) and comm[x] == "false."   :x +=1
    
        
    if x == len(comm):
        return None
    if comm[x] == "true.":
        return True
    
    pdst =""
    while x < len(comm) and comm[x][-1] ==",":
        x +=1 
        pdst += (comm[x] + "\n")

    pdst = comm[x]
    return pdst
    
    
def execSubstitutions():
    pass
    
def unify(t1, t2,substs):
    ct1 = t1.__class__
    ct2 = t2.__class__
    #print "ct1",ct1, "ct2",ct2
    if ( ct1 == ct2 ):
        
        #both Consts
        if (ct1 == Const ):
            if ( t1.name == t2.name):
                return
            
            raise UnificationError(t1,t2,0)
        
        if ( isinstance(t1, Relation) ):
            map( lambda x,y: unify(x,y, substs), t1.args, t2.args )
            return
            
        if (ct1==Var):
            raise UnificationError(t1,t2,"no vars allowed")
        
        if (ct1 == NotFormula ):
            unify(t1.f1,t2.f1,substs)
            return
        
    if (isinstance(t1,Relation) and isinstance(t2,Relation) ):
        raise UnificationError(t1,t2,1)
    
    
        
    if (isinstance(t2,Var) ):
        raise UnificationError(t1,t2,"no vars allowed")
        
    #print "t1 ",t1
    #print "t2 ",t2
    
    if (isinstance(t1,Var) ): 
        raise UnificationError(t1,t2,"no vars allowed")
        
        

    raise UnificationError(t1,t2,4)
         

def vars(t1):
    if ( isinstance(t1, NotFormula)):
        return vars(t1.f1)
    elif( isinstance(t1, Relation)):
        tab = map(vars, t1.args)
        return  sum(tab,[])
    elif( isinstance(t1, Var)):
        return [t1]
    elif ( isinstance(t1, Const)):
        return []  

if __name__ == '__main__':
    
    a = Const("a")
    b = Const("b")
    a_X =  sents_parse_string("a(X)", -1)[0]
    a_a =  sents_parse_string("a(a)", -1)[0]
    var = Var("Y")
 
    f= lambda x: sents_parse_string(x,-1)[0]
    
    x = f("b(X)")
    y = f("b(p)")
    
    t1 =[a,a_X] 
    t2 =[b,a_a]
    
    #print BrutefindUnify(t1, t2) 
    
    funny_tab = [(x,y),
#                 (a,a),
#                 (b,a),
#                 (a_X,a_a),
#                 (var,a),
#                 (var,a_X),
#                 (var,a_a),
                 ]
    funny_tab = map(lambda x: [ x, (x[1],x[0]) ], funny_tab)
    funny_tab = sum(funny_tab,[])
    print funny_tab
    
    for x in funny_tab:
        try:
            t1,t2 = x[0],x[1]
            substs =[]
            print "before"
            print t1,t2
            unify(t1, t2, substs)
            
            print substs
        except UnificationError as err:
            print "UnificationError "
            print err

            
    '''
    Random tests
    '''

    from test.RandomFromula import RandRelation    
    
    for x in xrange(1):
        t1 = a_X
        t2 = b
        #print t1
        #print t2
        pro =  BruteProgUnify([t1], [t2])
        try:
            substs =[]
            unify(t1, t2, substs)
            print substs
        except UnificationError as err:
            if pro:
                print "UnificationError " 
                print t1
                print t2
                print err
                print pro
                raise
            
        
    print "done"
    